COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00029 00003	.next page
C00058 ENDMK
C⊗;

.begin center
%3Runnable Specification As a Design Tool%2
.group skip 2
Ruth E. Davis
Electrical Engineering and Computer Science Department
University of Santa Clara
Santa Clara, CA 95053
.end
.group skip 6
%2There are at least four phases in the development of "correct" software.

1) Understanding the problem.  The program designer may work with intended
users of the system to develop an intuitive understanding of the problem and
possible approaches to its solution.

2) Formal specification.  Once the designer knows intuitively how to solve the
problem, the solution must be specified unambiguously.

3) Programming.  An implementation of the specification is programmed.

4) Verification.  The implementation developed in step three is shown to
satisfy the formal specification of step two.

There is a certain amount of testing and debugging that goes on at each of these
stages until one is satisfied with the current step and moves on to the next.
Several verification techniques have been developed to assist in accomplishing
step four.  However, even after a proof is completed we cannot claim to have
a "correct" program, only one that satisfies the given specification.

Rather than write a program, being guided by the specification, and then prove
it satisfies the specifications, one can automatically generate a program from
the specifications that is guaranteed to preserve the semantics, thus obviating
the need for the verification step entirely [1].

The truly creative (and most difficult) step in the development of a program
is the construction of an acceptable formal specification from an intuitive understanding
of the problem.  Thus, our efforts should be placed on developing design tools to
help with the construction and testing of the specification.  

How does one "debug" a specification?  We cannot hope to formally prove that a 
specification is "correct" with respect to our intuition, but we can at least test
it to see that it conforms to our intuition in specific cases.

Guttag and Horning [2] present an algebraic specification technique as a design
tool.  As an example they describe part of the specification of a high-level
interface to a flexible display and discuss the analysis of the specification.
A salient feature of their approach is the ability to "ask questions" of the
specification, derive answers, and change the design if the answers are
unacceptable.  In this way they hope to test and debug the specification.

I suggest that Horn clauses provide a much better specification language
than do algebraic axioms.  The two languages are closely related; it is
a simple matter to translate between them.  The ease of writing a specification
in one language versus the other is undoubtedly a matter of personal taste
and depends largely on which language one is more familiar with.  The same
may be said of the readability of a specification.  Horn clauses, as well as
algebraic axioms, can be analyzed for answers to specific questions and
modified accordingly.

The major distinction between the two methods is the manner in which questions
can be handled.  With the Guttag-Horning approach, an informal question is
posed and submitted to an "expert" who reformulates the question, often
generalizing it. The questioner must then be convinced that the formal statement
developed by the expert does indeed reflect the original question, and an 
answer to the formal question will provide an answer to the informal one.
Finally, an attempt is made to derive an answer from the axioms.

The same approach may be taken with Horn clauses, but it is not necessary.
Since Horn clauses are executable, if the questioner wants to know what happens
in a particular case, it is possible to simply "try it and see". The expert
will still be needed to develop the specification and to determine what modifications
should be made to the specification to change an unacceptable answer, but
the "what happens if ...?" questions no longer need be formalized.
For example, given the specification detailed in the appendix, and definitions
for the primitives (machine dependent) that interface the underlying logic with
the commands controlling the appearance of the screen, 
it is possible to execute logic programs that
manipulate the display.  Ideally, a "front-end" command language should be
provided by the designer(s) that enables users/testers of the design to
make their requests of the system without having to write them as Horn clauses.

Once one is satisfied that a Horn clause specification is a reasonable embodiment
of one's intuition, the task of refining the specification into an efficient
program can proceed. The ability to run a specification makes the problem of
testing and debugging it much more tractable.

As an example, I have written the Horn clause specification of the display
specified with algebraic axioms by Guttag and Horning.  The fundamental
assumption is that a user will want to be able to display several distinct
blocks of information on the screen at once.  The top level concept is
that of a %1view%2. A %1view%2 is a spatial arrangement of %1pictures%2; a
%1picture%2 is a block of displayable information. A picture consists of a
boundary, a contents, and a coordinate transformation to be applied in
viewing its contents. Examples of pictures are the entire display (with implicit
boundary), and the interior of a fixed rectangle on the display; examples of 
contents are text, figures, and views. Figure 1 is an example of a picture
(or a view containing a single picture).  Figure 2 presents a view containing
three pictures, each of which has the same contents; they differ in their
boundaries and the coordinate transformations applied in viewing their contents.

%2The Guttag-Horning specification of picture is as follows:
.begin nofill

%5Operators:

MakePicture: Contents %4X%5 [Coordinate → TruthValues] %4X%5 [Coordinate → Coordinate]
				 → Picture

Picture.Appearance: Picture %4X%5 Coordinate → Illumination

Picture.In: Picture %4X%5 Coordinate → TruthValues

Axioms:

Picture.Appearance(MakePicture(cont, bound, trans), coord) 
					%1=%5 Contents.Appearance(cont, trans(coord))

Picture.In(MakePicture(cont, bound, trans), coord) %1=%5 bound(coord)

.end
%2

The operators are listed first, giving their functionality, then the axioms defining
them are given.  %1MakePicture%2 is not defined further since it is simply the
constructor function for the type %1Picture%2.  The first axiom tells us that the
appearance at a given coordinate in a %1picture%2 is determined by the appearance
at a coordinate (the result of applying the transformation to the original
coordinate) in the %1contents%2 of the %1picture%2.  The second axiom indicates
that a coordinate is in a %1picture%2 if it is within the boundary of the %1picture%2
as defined by the function %1bound%2.

The specification of type %1Picture%2 using Horn clauses is given below. We distinguish
predicate names by capitalizing the first letter, constants and function symbols
are give in bold type, and variables are lower case italics. The Horn
clause specification clearly indicates the distinction between constructor functions,
such as %3make-picture%2, and the predicates indicating relationships among their
arguments. The type constraints, indicating functionality of the predicates, are
given only for the clause(s) defining the type being specified.
Type-checking can be included explicitly in each clause, however, we assume
the required type is made obvious by consistent naming of variables and
choose to leave it out of the rest of the
specification for the sake of readability.

.begin nofill

%5Picture(%7make-picture%*(cont, bound, trans)) ← Contents(cont), Boundary(bound),
						Translation(trans)

Picture-Appearance(%7make-picture%*(cont, bound, trans), coord, illum) ←
	Compute-position(coord, trans, coord'), Contents-appearance(cont, coord', illum)

Picture-In(%7make-picture%*(cont, bound, trans), coord, tv) ← Lies-in(coord, bound, tv)

.END 

In the Guttag-Horning axiomatic specification of the display, a %1boundary%2
is a function from %1Coordinate%2 to %1TruthValues%2 and a %1translation%2
is a function from %1Coordinate%2 to %1Coordinate%2.  Horn clause syntax does not
allow functions as arguments, thus I've treated %1trans%2 and %1bound%2 as objects,
%1Compute-position%2 is a predicate that accomplishes the translation from %1coord%2
to %1coord'%2 indicated by the Guttag-Horning %1trans%2, similarly, %1Lies-in(coord, bound, tv)%2
results in %1tv%2 being bound to %3true%2 if and only if the Guttag-Horning 
%1bound(coord)%2 is %3true%2, and to
%3false%2 if and only if Guttag-Horning %1bound(coord)%2 is %3false%2.  I would not
need the predicates %1Compute-position%2 and %1Lies-in%2 if I had an evaluation
predicate that accepts a function and its arguments and applies the function
to the arguments, such as the LISP "apply".  I have decided to remain within
first-order logic and the strict limitations of Horn clauses.  Others have
concerned themselves with the problem of moving to second-order, as shown in
the "demonstrate" predicate used of R. Kowalski and K. Bowen described in [3].

The specification of type %1View%2, given algebraically, is as follows:

.begin nofill

%5Operators:

View.Empty: → View

AddPicture: View %4X%5 Coordinate %4X%5 PictureId %4X%5 Picture → View

View.Appearance: View %4X%5 Coordinate → Illumination

View.In: View %4X%5 Coordinate → TruthValues

FindPictures: View %4X%5 Coordinate → IdList

DeletePicture: View %4X%5 PictureId → View

Axioms:

View.Appearance(AddPicture(v, coord', id, p), coord) %1=%5
		%6if%5 Picture.In(p, Minus(coord, coord'))
		%6then%5 Picture.Appearance(p, Minus(coord, coord'))
		%6else%5 View.Appearance(v, coord)

View.Appearance(View.Empty, coord)%6 intentionally left unspecified

%5View.In(View.Empty, coord) %1=%5 False

View.In(AddPicture(v, coord', id, p), coord) %1=%5 
			Picture.In(p, Minus(coord, coord')) ∨ View.In(v, coord)

FindPictures(View.Empty, coord) %1=%5 IdList.Empty

.group
FindPictures(AddPicture(v, coord', id, p), coord) %1=%5
		%6if%5 Picture.In(p, Minus(coord, coord'))
		%6then%5 IdList.Insert(id, FindPictures(v, coord))
		%6else%5 FindPictures(v, coord)
.apart

DeletePicture(View.Empty, id) %1=%5 View.Empty

DeletePicture( AddPicture(v, coord, id', p), id) %1=%5
		%6if%5 PictureId.Equal(id, id')
		%6then%5 v
		%6else%5 AddPicture(DeletePicture(v, id), coord, id', p)

.end

%2Guttag and Horning use the convention of prefixing a function name by the
type it is operating on and a dot.  In this way they can use the same name
for similar functions being defined over several different types.  They chose
to use a 0-ary function %1View.Empty%2 to indicate the empty view, we use a
constant %3mt-view%2. %1AddPicture%2 is the constructor function for type %1View%2.
%1Appearance%2 and %1In%2 are determined by the components (pictures) making up
a view.  %1FindPictures%2 is a function that constructs a list of %1id%2's of
pictures containing a given coordinate.  %1DeletePicture%2 deletes a picture,
specified by its %1id%2, from a view.

Again, using Horn clauses, we indicate the types of arguments only in the specification
of %1View%2, and assume the desired types are made apparent by naming of variables.

.begin nofill

%5View(%7mt-view%*) ←

View(%7add-picture%*(v, c, id, p)) ← View(v), Coordinate(c), PictureId(id), Picture(p)

View-Appearance(%7mt-view%*, coord, x) ←

%6As in the algebraic specification, we leave unspecified the appearance of the 
%7mt-view%6 at any coordinate.  Since we have no if-then-else, the axiom describing 
%5View.Appearance%6 corresponds to two Horn clauses, one for each alternative.%5

View-Appearance(%7add-picture%*(v, coord', id, p), coord, illum) ←
				Picture-In(p, %7minus%*(coord, coord'), %7true%*),
				Picture-Appearance(p, %7minus%*(coord, coord'), illum)

View-Appearance(%7add-picture%*(v, coord', id, p), coord, illum) ←
				Picture-In(p, %7minus%*(coord, coord'), %7false%*),
				View-Appearance(v, coord, illum)

View-In(%7mt-view%*, coord, %7false%*) ←

%6Horn clauses are not allowed alternative conditions. Thus the second axiom for 
%5View.In%6 is handled by the following three Horn clauses, one for each alternative
making the conclusion %7true%6, and a third to enable us to derive the fact that a 
coordinate is not in a %5view%6.

.group
%5View-In(%7add-picture%*(v, coord', id, p), coord, %7true%*) ←
				Picture-In(p, %7minus%*(coord, coord'), %7true%*)
.apart

View-In(%7add-picture%*(v, coord', id, p), coord, %7true%*) ← View-In(v, coord, %7true%*)

View-In(%7add-picture%*(v, coord', id, p), coord, %7false%*) ←
				Picture-In(p, %7minus%*(coord, coord'), %7false%*),
				View-In(v, coord, %7false%*)

FindPictures(%7mt-view%*, coord, %7mt-idlist%*) ←

FindPictures(%7add-picture%*(v, coord', id, p), coord, %7idlist-insert%*(id,idl)) ←
				Picture-In(p, %7minus%*(coord, coord'), %7true%*),
				FindPictures(v, coord, idl)

FindPictures(%7add-picture%*(v, coord', id, p), coord, idl) ←
				Picture-In(p, %7minus%*(coord, coord'), %7false%*),
				FindPictures(v, coord, idl)

DeletePicture(%7mt-view%*, id, %7mt-view%*) ←

DeletePicture(%7add-picture%*(v, coord, id, p), id, v) ←

DeletePicture(%7add-picture%*(v, coord, id', p), id, %7add-picture%*(v', coord, id', p)) ←
				PictureId-equal(id, id', %7false%*), DeletePicture(v, id, v')

.end
%1FindPictures%2 and %1DeletePicture%2 present no surprises.  Again, an if-then-else
in an axiom results in two clauses in the Horn clause specification.
A complete Horn clause specification of the display is given in the appendix.


In analyzing the specification using the algebraic axioms one needs an expert to
go between the questioner and the specification.  For example, and informal question
asked of Guttag and Horning was: "Is it the case that pictures are not transparent
or even translucent? I.e., if two pictures overlap, does the bottom one have no
effect on what one sees through the top one?". The alternatives are pictured in
Figures 3a and 3b. The question was formalized as:
.begin nofill

"Is it true that      
%5(∀c, c', w, id, v1, v2)[Picture.In(w, Minus(c, c')) →
.fp
   [View.Appearance(AddPicture(v1, c', id, w), c) %1=%5 View.Appearance(AddPicture(v2, c', id, w), c)]] %6?"

.end
%2The formal question is answered affirmatively, following directly from the first
alternative in the first axiom of type %1View%2.

If we so desired, we could formalize the question to be put to our Horn clause
specification and derive the same answer, using the second clause in the definition
of %1View-Appearance%2, but there is no need.  Since we can run the Horn clause
specification, all the user need do is construct overlapping pictures and look
at the result. This is sufficient to answer questions about specific cases.
If one is interested in proving general properties, then we must fall back to
a formalization of the question and formal derivation of an answer from the
specification. In order to accomplish this derivation, we often need the "closed
world" assumption, that is, we assume that the specification is complete.  For
the current example, the question is formalized as:
.begin nofill

"Is it true that
%5View-Appearance(%7add-picture%*(v1, c', id, p), c, illum) ←
	Picture-In(p, %7minus%*(c, c', %7true%*),
	View-Appearanc(%7add-picture%*(v2, c', id, p), c, illum) %6?"

.end
%2By assuming the "only-if" direction of the first clause in the definition of
%1View-Appearance%2, which is clearly the intent of the definition, we can derive
that %1Picture-Appearance(p, %3minus%*(c, c'), illum)%2. Then using the same clause,
exactly as stated, we derive the result.

Using Horn clauses as a design tool we enjoy all the benefits of the algebraic
approach, and gain the advantage that testing is more easily accomplished.  An
expert may still be required to develop the design specification and to modify it if
necessary, but the analysis of the design can be carried out by people who may be 
experts in the problem domain but not in the specification language.

.group skip 2
.center
%3References%2
.group skip 1
.nofill
[1] Davis, R. E., "Generation of Correct Programs from Logic Specifications",
		Ph.D. Thesis, Board of Information Sciences, University of 
		California, Santa Cruz, 1979.

.group
[2] Guttag, J., and J. Horning, "Formal Specification As a Design Tool", 
		Proceedings of the ACM Symposium on Principles of Programming
 		Languages, 1980.
.apart

[3] Kowalski, R., %1Logic for Problem Solving%2, Elsevier North Holland, Inc., 1979.


.next page
.GROUP skip 1
.begin center
%3Appendix%5
.end
.nofill
.group skip 1
%5TYPE Picture

Picture(%7make-picture%*(cont, bound, trans)) ← 
	Contents(cont), Boundary(bound), Translation(trans)

Picture-Appearance(%7make-picture%*(cont, bound, trans), coord, illum) ←
	Compute-position(coord, trans, coord'), Contents-appearance(cont, coord', illum),
	Contents(cont), Boundary(bound), Translation(trans), Coordinate(coord),
	Coordinate(coord'), Illumination(illum)

Picture-In(%7make-picture%*(cont, bound, trans), coord, tv) ←
	Lies-in(coord, bound, tv), Contents(cont), Boundary(bound),
	Translation(trans), Coordinate(coord), Truth-value(tv)

END TYPE Picture

TYPE Contents

Contents(%7mt-contents%*) ←

Contents(%7add-component%*(cont, comp, coord)) ← Contents(cont), Component(comp), Coordinate(coord)

Contents-Appearance(%7mt-contents%*, coord, x) ←

%6The appearance of an empty contents at a coordinate is intentionally left unspecified as yet.%5

.group
Contents-Appearance(%7add-component%*(cont, comp, coord'), coord, illum) ←
	Component-In(comp, %7minus%*(coord, coord'), %7true%*),	Contents-In(cont, coord, %7true%*),
	Component-Appearance(comp, %7minus%*(coord, coord'), illum1),
	Contents-Appearance(cont, coord, illum2), Combine(illum1, illum2, illum)
.apart

.group
Contents-Appearance(%7add-component%*(cont, comp, coord'), coord, illum) ←
	Component-In(comp, %7minus%*(coord, coord'), %7true%*), Contents-In(cont, coord, %7false%*),
	Component-Appearance(comp, %7minus%*(coord, coord'), illum)
.apart

Contents-Appearance(%7add-component%*(cont, comp, coord'), coord, illum) ←
	Component-In(comp, %7minus%*(coord, coord'), %7false%*), Contents-Appearance(cont, coord, illum)

Contents-In(%7mt-contents%*, coord, %7false%*) ←

.group
Contents-In(%7add-component%*(cont, comp, coord'), coord, %7true%*) ← 
	Component-In(comp, %7minus%*(coord, coord'), %7true%*)
.apart

Contents-In(%7add-component%*(cont, comp, coord'), coord, %7true%*) ← Contents-In(cont, coord, %7true%*)

.group
Contents-In(%7add-component%*(cont, comp, coord'), coord, %7false%*) ←
	Component-In(comp, %7minus%*(coord, coord'), %7false%*), Contents-In(cont, coord, %7false%*)
.apart

END TYPE Contents
.next page

TYPE Component 
%6Simply the union of %5View, Text%6, and %5Figure.%5

Component(%7make-vcomp%*(view)) ←

Component(%7make-tcomp%*(text)) ←

Component(%7make-fcomp%*(figure)) ←

Component-Appearance(%7make-vcomp%*(view), coord, illum) ←
	View-Appearance(view, coord, illum)

Component-Appearance(%7make-tcomp%*(text), coord, illum) ←
	Text-Appearance(text, coord, illum)

Component-Appearance(%7make-fcomp%*(figure), coord, illum) ←
	Figure-Appearance(figure, coord, illum)

Component-In(%7make-vcomp%*(view), coord, tv) ← 
	View-In(view, coord, tv)

Component-In(%7make-tcomp%*(text), coord, tv) ← 
	Text-In(text, coord, tv)

Component-In(%7make-fcomp%*(figure), coord, tv) ← 
	Figure-In(figure, coord, tv)

END TYPE Component

.next page
TYPE View

View(%7mt-view%*) ←

View(%7add-picture%*(view, coord, picture-id, picture)) ←

View-Appearance(%7mt-view%*, coord, x) ←

%6Again, we leave unspecified the appearance 
of the %5mt-view%6 at any coordinate%5

.group
View-Appearance(%7add-picture%*(v, coord', id, p), coord, illum) ←
	Picture-In(p, %7minus%*(coord, coord'), %7true%*),
	Picture-Appearance(p, %7minus%*(coord, coord'), illum)
.apart

.group
View-Appearance(%7add-picture%*(v, coord', id, p), coord, illum) ←
	Picture-In(p, %7minus%*(coord, coord'), %7false%*),
	View-Appearance(v, coord, illum)
.apart

View-In(%7mt-view%*, coord, %7false%*) ←

View-In(%7add-picture%*(v, coord', id, p), coord, %7true%*) ←
	Picture-In(p, %7minus%*(coord, coord'), %7true%*)

View-In(%7add-picture%*(v, coord', id, p), coord, %7true%*) ←
	View-In(v, coord, %7true%*)

View-In(%7add-picture%*(v, coord', id, p), coord, %7false%*) ←
	Picture-In(p, %7minus%*(coord, coord'), %7false%*),
	View-In(v, coord, %7false%*)

FindPictures(%7mt-view%*, coord, %7mt-idlist%*) ←

FindPictures(%7add-picture%*(v, coord', id, p), 
		coord, %7idlist-insert%*(id, idl)) ←
	Picture-In(p, %7minus%*(coord, coord'), %7true%*),
	FindPictures(v, coord, idl)

FindPictures(%7add-picture%*(v, coord', id, p), coord, idl) ←
	Picture-In(p, %7minus%*(coord, coord'), %7false%*),
	FindPictures(v, coord, idl)

DeletePicture(%7mt-view%*, id, %7mt-view%*) ←

DeletePicture(%7add-picture%*(v, coord, id, p), id, v) ←

DeletePicture(%7add-picture%*(v, coord, id', p), 
		id, %7add-picture%*(v', coord, id', p)) ←
	PictureId-equal(id, id', %7false%*),
	DeletePicture(v, id, v')

END TYPE View

.next page
TYPE Idlist

Idlist(%7mt-idlist%*) ←

Idlist(%7idlist-insert%*(id, idl)) ←
		 PictureId(id), Idlist(idl)

END TYPE Idlist

TYPE Text

Text(%7mt-text%*) ←

Text(%7text-insert%*(par, txt)) ← Paragraph(par), Text(txt)

%6macro: %5down(d)%6 is %5minus(coord, times(d, %7unitvectordown%*) 

Text-Appearance(%7mt-text%*, coord, x) ←

Text-Appearance(%7text-insert%*(par, txt), coord, illum) ←
	Paragraph-In(par, coord, %7true%*),
	Paragraph-Appearance(p, coord, illum)

Text-Appearance(%7text-insert%*(par, txt), coord, illum) ←
	Paragraph-In(par, coord, %7false%*), 
	Paragraph-Height(par, d),
	Text-Appearance(txt, %7down%*(d), illum)

Text-In(%7mt-text%*, coord, %7false%*) ←

Text-In(%7text-insert%*(par, txt), coord, %7true%*) ← 
	Paragraph-In(par, coord, %7true%*)

Text-In(%7text-insert%*(par, txt), coord, %7true%*) ←
	Paragraph-Height(par, d), 
	Text-In(txt, %7down%*(d), %7true%*)

Text-In(%7text-insert%*(par, txt), coord, %7false%*) ←
	Paragraph-In(par, coord, %7false%*),
	Paragraph-Height(par, d), 
	Text-In(txt, %7down%*(d), %7false%*)

END TYPE Text

.next page
TYPE Paragraph   
%6macro: %7down%*(d) is %7minus%*(coord, %7times%*(d, %7unitvectordown%*) %5

Paragraph(%7make-paragraph%*(parlooks, eng-string)) ←

Par-Firstline(%7make-paragraph%*(look, s), line) ←
	Parlooks-width(look, w),
	EngString-Firstline(s, w, line)

Par-Balance(%7make-paragraph%*(look, s), 
	     %7make-paragraph%*(look, s')) ←
	Parlooks-width(look, w),
	EngString-Balance(s, w)

Par-Null(%7make-paragraph%*(look, s), tv) ← 
	String-Null(s, tv)

Par-Space(%7make-paragraph%*(look, s), dist) ←
		ParLooks-space(look, dist)

.group
Par-Height(p, dist) ← 
	Par-Null(p, %7true%*), Par-Space(p, dist)
.apart

.group
Par-Height(p, dist1 + dist2) ← Par-Null(p, %7false%*),
	Par-Firstline(p, line), Line-Height(line, dist1),
	Par-Balance(p, p'), Par-Height(p', dist2)
.apart

.group
Par-In(p, coord, %7true%*) ← Par-Null(p, %7false%*),
	Par-Firstline(p, line), Par-Space(p, dist1),
	Line-Ascent(line, dist2), 
	Line-In(line, %7down%*(dist1 + dist2), %7true%*)
.apart

Par-In(p, coord, %7true%*) ← Par-Null(p, %7false%*),
	Par-Balance(p, p'), Par-Firstline(p, line),
	Line-Height(line, dist), Par-In(p', %7down%*(dist), %7true%*)

Par-In(p, coord, %7false%*) ← Par-Null(p, %7true%*)

Par-In(p, coord, %7false%*) ← Par-Null(p, %7false%*),
	Par-Firstline(p, line), Par-Space(p, dist1),
	Line-Ascent(line, dist2), Par-Balance(p, p'), 
	Line-In(line, %7down%*(dist1 + dist2), %7false%*),
	Line-Height(line, dist), Par-In(p', %7down%*(dist), %7false%*)

Par-Appearance(p, coord, illum) ←
	Par-Firstline(p, line), Par-Space(p, dist1),
	Line-Ascent(line, dist2), 
	Line-In(line, %7down%*(dist1 + dist2), %7true%*), 
	Line-Appearance(line, %7down%*(dist1 + dist2), illum)

Par-Appearance(p, coord, illum) ←
	Par-Firstline(p, line), Par-Space(p, dist1),
	Line-Ascent(line, dist2), 
	Line-In(line, %7down%*(dist1 + dist2), %7false%*),
	Par-Balance(p, p'), Line-Height(line, dist), 
	Par-Appearance(p', %7down%*(dist), illum)

END TYPE PARAGRAPH

.next page
TYPE EnglishString

EngString(%7mt-string%*) ←

EngString(%7string-insert%*(char, string) ← 
	Character(char), EngString(string)

EngString-Firstline(%7mt-string%*, dist, %7mt-line%*) ←

.group
EngString-Firstline(%7string-insert%*(c, s), d, c) ← 
	SplitHere(s, c, d, %7true%*)
.apart

.group
EngString-Firstline(%7string-insert%*(c, s), d, 
			%7line-insert%*(c, line)) ←
	SplitHere(s, c, d, %7false%*), Character-width(c, w),
	EngString-Firstline(s, d-w, line)
.apart

EngString-Balance(%7mt-string%*, d, %7mt-string%*)←

EngString-Balance(%7string-insert%*(c, s), d, s) ←
	SplitHere(s, c, d, %7true%*)

EngString-Balance(%7string-insert%*(c, s), d, str) ←
	Character-width(c, w), EngString-Balance(s, d-w, str)

SplitHere(%7mt-string%*, c, d, %7true%*) ←

SplitHere(%7string-insert%*(c', s), c, d, %7true%*) ← 
	Character-Equal(c', %7return%*, %7true%*)

SplitHere(%7string-insert%*(c', s), c, d, %7true%*) ← 
	Character-Equal(c', %7space%*, %7false%*),
	Character-width(c, w), Character-width(c', w'),
	LessThan(d, w+w', %7true%*)

SplitHere(%7string-insert%*(c', s), c, d, %7true%*) ← 
	LexicalBreak(c, c', %7true%*), Character-width(c, w),
	WordFits(s, c', d-w, %7false%*)

SplitHere(%7string-insert%*(c', s), c, d, %7false%*) ←
	Character-Equal(c', %7return%*, %7false%*),
	Character-Equal(c', %7space%*, tv1), 
	Character-width(c, w), Character-width(c', w'),
	LessThan(d, w+w', tv2), Not(tv2, tv2'),
	Or(tv1, tv2', %7true%*),
	LexicalBreak(c, c', tv3), Not(tv3, tv3'),
	Character-width(c, w), WordFits(s, c', d-w, tv4),
	Or(tv3', tv4, %7true%*)

Not(%7true%*, %7false%*) ←

Not(%7false%*, %7true%*) ←

Or(%7true%*, tv, %7true%*) ←

Or(tv, %7true%*, %7true%*) ←

Or(%7false%*, %7false%*, %7false%*) ←

.group
LexicalBreak(current, next, %7true%*) ←
	Character-Equal(current, %7space%*, %7true%*),
	Character-Equal(next, %7space%*, %7false%*)
.apart

.group
LexicalBreak(current, next, %7true%*) ←
	Character-Equal(current, %7hyphen%*, %7true%*),
	Character-Equal(next, %7hyphen%*, %7false%*),
	Character-Equal(next, %7space%*, %7false%*)
.apart

.group
LexicalBreak(current, next, %7false%*) ←
	Character-Equal(next, %7space%*, %7true%*)
.apart

.group
LexicalBreak(current, next, %7false%*) ←
	Character-Equal(current, %7space%*, %7false%*),
	Character-Equal(current, %7hyphen%*, %7false%*)
.apart

.group
LexicalBreak(current, next, %7false%*) ←
	Character-Equal(current, %7space%*, %7false%*),
	Character-Equal(next, %7hyphen%*, %7true%*),
.apart

WordFits(%7mt-string%*, c, d, %7true%*) ←

WordFits(%7string-insert%*(c', s), c, d, %7true%*) ← 
	Character-Equal(c, %7return%*, %7true%*)

WordFits(%7string-insert%*(c', s), c, d, %7true%*) ← 
	Character-Equal(c, %7space%*, %7true%*)

WordFits(%7string-insert%*(c', s), c, d, %7true%*) ← 
	LexicalBreak(c, c', %7true%*), Character-width(c, w),
	LessThan(d, w, %7false%*)

WordFits(%7string-insert%*(c', s), c, d, %7true%*) ← 
	Character-width(c, w), Character-width(c', w'),
	LessThan(d, w+w', %7false%*),
	WordFits(s, c', d-w, %7true%*)

WordFits(%7string-insert%*(c', s), c, d, %7false%*) ←
	Character-Equal(c, %7return%*, %7false%*),
	Character-Equal(c, %7space%*, %7false%*),
	LexicalBreak(c, c', tv1), Not(tv1, tv1'),
	Character-width(c, w), LessThan(d, w, tv2),
	Or(tv1', tv2), Character-width(c', w'),
	LessThan(d, w+w', tv3),
	WordFits(s, c', d-w, tv4), Not(tv4, tv4'),
	Or(tv3, tv4', %7true%*)

String-Null(%7mt-string%*, %7true%*) ←

String-Null(%7string-insert%*(c, s), %7false%*) ←

END TYPE EnglishString

.next page
TYPE LINE

Line(%7mt-line%*) ←

Line(%7line-insert*(c, l)) ← Character(c), Line(l)

.group
%5Line-Appearance(%7mt-line%*, coord, illum)%6 
   intentionally left unspecified
.apart
macro: %5Right(d)%6 is %5Minus(coord, %7times%*(d, %7unitvectorright%*)  

.group
Line-Appearance(%7line-insert*(c, ln), coord, illum) ←
	Character-In(c, coord, %7true%*),
	Character-Appearance(c, coord, illum)
.apart

Line-Appearance(%7line-insert*(c, ln), coord, illum) ←
	Character-In(c, coord, %7false%*), Character-width(c, w),
	Line-Appearance(ln, %7right%*(w), illum)

Line-In(%7mt-line%*, coord, %7false%*) ←

Line-In(%7line-insert*(c, ln), coord, %7true%*) ←
	Character-In(c, coord, %7true%*)

Line-In(%7line-insert*(c, ln), coord, %7true%*) ←
	Character-width(c, w),
	Line-In(ln, %7right%*(w), %7true%*)

Line-Height(ln, d1+d2) ←
	Line-Ascent(ln, d1), Line-Descent(ln, d2)

Line-Ascent(%7mt-line%*, 0) ←

Line-Ascent(%7line-insert*(c, ln), d) ←
	Character-Ascent(c, d1), Line-Ascent(ln, d2),
	Maximum(d1, d2, d)

Line-Descent(%7mt-line%*, 0) ←

Line-Descent(%7line-insert*(c, ln), d) ←
	Character-Descent(c, d1), Line-Descent(ln, d2),
	Maximum(d1, d2, d)

Maximum(x, y, x) ← LessThan(x, y, %7false%*)

Maximum(x, y, y) ← LessThan(y, x, %7false%*)

%6I have assumed the existence of a %5LessThan%6
 predicate that returns %5true%6 or %5false%5

END TYPE LINE

.next page
.group
TYPE Character

Character(%7make-char%*(code, fig, ascent, descent, width)) ←
	CharacterCode(code), Figure(fig), Distance(ascent),
	Distance(descent), Distance(width)
.apart

.group
Character-width(%7make-char%*(code, fig, ascent, 
				descent, width), width) ←
.apart

.group
Char-equal(%7make-char%*(code, fig, asc, des, w),
	   %7make-char%*(code', fig', asc', des', w')) ←
	CharacterCode-Equal(code, code', %7true%*)
.apart

.group
Character-Ascent(%7make-char%*(code, fig, ascent, 
				descent, width), ascent) ←
.apart

Character-Descent(%7make-char%*(code, fig, ascent, 
				descent, width), descent) ←

Char-Appearance(%7make-char%*(cd, f, a, d, w), coord, illum) ←
	Figure-Appearance(f, coord, illum)

Char-In(%7make-char%*(cd, f, a, d, w), coord, %7true%*) ←
	Figure-In(f, coord, %7true%*),
	Increasing(a, %7project%*(coord, %7unitvectordown%*), d, %7true%*),
	Increasing(0, %7project%*(coord, %7unitvectorright%*), w, %7true%*)

Char-In(%7make-char%*(cd, f, a, d, w), coord, %7false%*) ←
	Figure-In(f, coord, %7false%*)

Char-In(%7make-char%*(cd, f, a, d, w), coord, %7false%*) ←
	Increasing(a, %7project%*(coord, %7unitvectordown%*), d, %7false%*)

Char-In(%7make-char%*(cd, f, a, d, w), coord, %7false%*) ←
	Increasing(0, %7project%*(coord, %7unitvectorright%*), w, %7false%*)

END TYPE Character
.next page
TYPE Figure

%6Type %5Figure%6 will necessarily include specifications 
of the %5Appearance%6 and %5In%6 predicates for the type. 
This type is left unspecified as it may be dependent upon
the target system.  Clearly, a more flexible specification 
of %5Figure%6 is possible for a bit mapped display than is 
possible given a character mapped display. %5

END TYPE Figure

TYPE Coordinate

%6 This type is not yet specified. It needs at least the 
functions %7minus%*, %7times%*, %6and %7project%6, and the constants 
%7unitvectorright%6 and %7unitvectordown%6.  A 2-dimensional
vector space would do, and one might consider this a 
primitive type of the system one is using.%5

END TYPE Coordinate

TYPE Distance

%6 Again, this type should be available already on the 
target system.  One simply needs to define the mapping 
from the predicate form used in the Horn clauses to
the functions available.%5

END TYPE Distance

TYPE Font

Font(%7mt-font%*) ←

Font(%7add-character%*(font, char)) ←

Lookup(%7mt-font%*, code, x) ← 
%6another unspecified pathological case%5

Lookup(%7add-character%*(fnt, %7make-char%*(cd, f, a, d, w)),
		     cd, %7make-char%*(cd, f, a, d, w)) ←

Lookup(%7add-character%*(fnt, %7make-char%*(cd, f, a, d, w)), code, c) ←
	CharacterCode-Equal(cd, code, %7false%*),
	Lookup(fnt, code, c)

END TYPE Font

PRIMITIVES

%6The primitive predicates that relate the logic to a 
particular system include the types %5Boundary, Translation,
Coordinate, Illumination,%6 and the predicates, such as 
%5Compute-Position, Lies-In,%6 and %5Minus%6, that operate 
on them. For example, an %5illumination%6 may be one of two 
values (white/black), one of several shades of grey, or a 
more complex combination of hue and intensity, depending 
on the capabilities of the system one is designing.